T:Type, L:(T List). (x:T. (x  L))  (0 < ||L||) 

latex

ProofTree

Definitions	A  B, i  j , a < b, x:AB(x), P  Q, P  Q, x:A  B(x), P & Q, P  Q, Type, type List, x:A. B(x), s = t, A, ||as||, #$n, (x  l), x:A. B(x)
Lemmas	l member wf, member-exists, not wf, iff functionality wrt iff, length of not nil, iff wf, rev implies wf, ge wf